COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\J	At present a large part of our work in mathematical theory of
C00022 ENDMK
C⊗;
\J	At present a large part of our work in mathematical theory of
computation and in the representation problem in artificial intelligence
is focussed on improving and using the FOL proof-checker for first order
logic.  This confluence is undoubtedly temporary, and the two projects
will diverge again in a year or so.

	From the artificial intelligence point of view the work using FOL
is a subproblem of a subproblem, and it we should probably say something
about why we are doing it this way.  Of course, almost everyone is working
on pieces of the AI problem, but we are dividing the problem horizontally
rather than vertically.  The distinction is that the in the usual vertical
subdivision, one will take a particular problem such as chess or natural
language dialog in a restricted area and write a complete program to
exhibit intelligence there.  The horizontal subdivision involves taking
an aspect of intelligence and studying that.  Our present work is based
on the subdivision of the AI problem into heuristic and epistemological
parts and studying the epistemological part.  In particular, we are interested
in the reasoning whereby it is established that a strategy is appropriate
for achieving a goal.  We are interested in cases of this where the human
reasoning is quite clear informally, and we are studying how to formalize
this reasoning in first order logic.

	So far we have reached the following conclusions and obtained the
following results.

	1. In general, first order logic is an appropriate vehicle assuming
that set theory is used so that functions and predicates can be replaced
by individuals in sets of mappings whenever their properties have to be
discussed.

	2. The logic requires several forms of supplementation in order
to express the reasoning humans actually carry out.

	3. Much human mathematical reasoning is actually metamathematical.
In order to express it formally, we must use formalisms that can discuss
their own metamathematics.  We are doing it, but some more elementary
parts of the system have to be put in good order first.

	4. Besides the reasoning that corresponds to the steps in a first
order proof, humans do a lot of reasoning that corresponds to to simple
calculation, i.e. properties of the external problem or of the formulas
themselves are observed directly or computed rather than generated step
by step from some kind of atomic sentences expressing observations.  However,
the logical reasoning that is expressible in terms of application of
rules of inference also plays a key role.  Therefore, we have added to
our logical system the ability to assert that a LISP function computes
a certain function or predicate and to generate assertions by computation
whenever the arguments of the functions are available as constants.

	5. These aspects of reasoning


THE FORMAL EXPRESSION OF HUMAN REASONING


	The Mathematical Theory of Computation Group and the Representation
Group are currently united in developing ways of expressing human reasoning
about mathematical proofs, the correctness of programs, and the appropriateness
of a strategy for achieving a goal in terms acceptable to a proof-checker
called FOL.  The work involves developing FOL so that it will accept reasoning
in a form that seems closer to that we might be able to generate as well as
have the ability to express large proofs of important results in FOL.  For
the moment we shall put off explaining why this is an appropriate way of 
attacking the AI problem and will concentrate on explaining what we are doing,
what we have accomplished so far, and what we expect to accomplish in the next 
two years.

	FOL is a proof-checker for first order logic supplemented by features
intended to make human reasoning translatable statement-by-statement into 
reasoning acceptable to the proof-checker.  To avoid misunderstanding, we 
should say that almost all the proofs that interest us use set theory within 
the logic so that functions and predicates can effectively be objects when 
this is wanted as it often is.

	FOL is based on the "natural deduction" style of representing the
derivations of the theorems of first order logic.  The existing supplements,
over and above Prawitz's description of the underlying formal system, include
the following:

	1. A decision procedure for tautological reasoning that allows
any purely propositional reasoning to be carried out in one step.  This
procedure has proved entirely practical giving an answer in a short time
even when there are tens of premisses and tens of variables.

	2. A partial proof procedure for reasoning with equality.  It has
proved quite useful even though its capabilities are limited.

	3. The introduction of sort restrictions on the range of variables.
This, for example, allows a user to "for all pawns ...", rather than "for
all X, if X is a pawn then ...".

	4. The ability to attach a LISP function to a function or
predicate symbol in the logic and to generate sentences by evaluating
expressions.  The importance of this comes from the fact that human
reasoning is not purely logical but involves observation and computations
that are not succinctly expressable as the application of rules of
inference.

	4. A start has been made on formalizing metamathematics of FOL
based languages within FOL.

	5. A powerful rule for manipulating quantifiers has been implemented
that does certain complex chains of reasoning in a single step.  This rule is
essential for the proposed introduction of subgoaling facilities similiar to 
those in LCF.

	Much of our previous work on formalizing proofs of the correctness
of computer programs has been based on a proof-checker called LCF for a 
logic of Robin Milner based on a logic of Dana Scott.  Within this 
formalism a number of programs were proved correct including some simple
compilers and an interpreter for LISP.  In the course of this work, some
limitations of LCF turned up, but LCF has many features for making proofs
easier that have yet to be incorporated in FOL, because FOL is a more 
complicated logical environment.  Our preliminary experience with FOL 
showed that it had to be substantially rewritten.  This took a lot of time, 
but the new version is now in a usable state.

	The first substantial tasks that have been undertaken with FOL
are the verification of theorems in elementary number theory.  Even this
illustrates that much of ordinary mathematical reasoning is metamathematical
and that the axiomatic formalisms ordinarily proposed are not adequate to
express the proofs that are actually made.  In fact the usual axiomatic
formalisms are adequate only in the sense that it is possible to prove
informally that formal proofs exist, but the formal proofs to not express
the informal reasoning.  We are gradually correcting this by making the
proofs and modifying both FOL and our axiom systems so that they informal
reasoning can be well expressed.  The ability to carry out metamathematical 
reasoning within FOL, and how to do this is one of will be an active topic 
of research.

	The mathematical tools for expressing the Scott formalism on which 
LCF is based in FOL are being developed, but the formalism has not yet 
reached the point where proofs are being written.

	Our first major attempt to express non-mathematical reaoning has
been to prove that certain chess problems have the stated solutions.  If
the reasoning had involved merely following out a part of the move tree
as is adequate for many chess problems, the formalization problem would
have been trivial.  However, in the examples we have chosen, a simple
tree search does not correspond to the human reasoning.  Instead it is
necessary to argue about what one player is doing while another follows
a certain path in general terms, because tree search would be too long
and is unnecessary because the different possible moves have similar effects.
In the chess reasoning, it has been found that only a part (albeit an
important part) of the reasoning is appropriately carried out in logic.
The rest is based on direct observation of chess boards or direct tree
search and is appropriately carried out by programs attached to function
symbols as mentioned above.

	In the next two years, it looks like we can be much more ambitious
in terms of externally visible accomplishment than we have been in the
last few years, because we are finally getting out of the grubby system
building stage and will be able to put more resources into major extensions
of FOL and especially into the use of FOL rather than having to concentrate
on civilizing it.  Here are our goals:

	1. Express some major mathematical proofs.  Examples in increasing
estimated difficulty include

		a. The standard set-theoretic proof of Wilson's theorem.

		b. Difficult combinatorial theorems like Ramsey's theorem
or van der Waerden's theorem on arithmetic progressions in partitions of
the integers into sets.  When we can do these, we will have shown our
ability to express mathematical reasoning of the complexity that occurs
in research papers.

		c. The formalization of the reasoning in Cohen's "Set Theory
and the Continuum Hypothesis".  This reasoning is heavily metamathematical,
and expressing it will require a good formalization of metamathematics.

	We target these tasks at three months, six months and eighteen
months, and there is a substantial probability that we will be diverted
from the last by something else coming to appear more appropriate.  By the
end of the next contract period, we expect that FOL will be in a state
where the reasoning in a mathematical paper can be expressed in a
straightforward way by someone who understands the paper.

	2. Express a version of the Scott logic in FOL and prove sample
interpreters, compilers and application programs correct.  The formalization
should take another six months and then the applications should begin
to flow.

	3. Finish the chess reasoning problems now being worked on and get
a good formalization of parallel action.  It is difficult to say how long
this last task will take.

	4. The following features are expected to be added to the FOL system.

		a. goal structure similiar to the existing features in LCF.
		b. MFOL - i.e. the ability to do the metamathematical 
		   reasoning discussed above.  This might include the ability
	   	   of the user to prepare and call upon proof generating 
		   subroutines so that FOL will gradually become a theorem 
		   prover as well as a proof-checker.
		c. an extensive definitional facility.  This corresponds
		   to the usual mathematical practice of defining new 
		   notions and then operating with them in a valid way.
		d. a badly needed theorem making and using facility.  At
		   present there is no way to create a theorem, which could
		   be used later in another proof.

This will probably take six to nine months at the present rate of progress.
	
	Now that we have explained what we plan to do, it is worthwhile to
say something about why the approach seems appropriate in the present state
of artificial intelligence research.  The AI problem has always been regarded
as difficult, and it has always been appropriate to find good subproblems.
Mostly this has been done by making complete systems like theorem provers
or chess programs or question answerers and restricting the domain of
operation of the system or settling for limited performance.  This might
be called a vertical subdivision of the AI problem.

	Vertical subdivision of the problem is appropriate, but so is
horizontal subdivision which concentrates on an aspect of intelligence.
In the present case, we are relying on the division of the AI problem into
the heuristic part and the epistemological part as proposed in
(McCarthy and Hayes 1970), and the present work is on the epistemological
part.  Thus in mathematics, we are concentrating on being able to express
formally the reaoning that is actually made in the hope that success therein
will provide a basis for programs that can generate real mathematical
proofs.